.require "memo.pub[let,jmc]" source;
.turn off "_"
.font C "zero30"
.at "Goedel" ⊂"G%C:%*odel"⊃
.at "qF" ⊂"%AF%*"⊃
.cb "ADDENDUM: CIRCUMSCRIPTION AND OTHER NON-MONOTONIC FORMALISMS"

	Circumscription and
the non-monotonic reasoning
formalisms of McDermott and Doyle (1980) and Reiter (1980) differ along
two dimensions.  First, circumscription is concerned with minimal
models, and they are concerned with arbitrary models.
It appears that these approaches solve somewhat different though
overlapping classes of problems, and each has its uses.  The other
difference is that the reasoning of both other formalisms
involves models directly, while the syntactic formulation of
circumscription uses axiom schemata.  Consequently, their systems
are incompletely formal unless the metamathematics is also formalized.
and this hasn't yet been done.

	However, schemata are applicable to other formalisms
than circumscription.  Suppose, for example, that we have some axioms about
trains and their presence on tracks, and we wish to express the fact
that if a train may be present, it is unsafe to cross the tracks.
In the McDermott-Doyle formalism, this might be expressed

!!a1:	%2M on(train,tracks) ⊃ ¬safe-to-cross(tracks)%1,

where the properties of the predicate %2on%1 are supposed
expressed in a formula that we
may call %2Axiom(on)%1.  The %2M%1 in ({eq a1}) stands for "is
possible".
We propose to replace ({eq a1}) and %2Axiom(on)%1 by
the schema

!!a2:	%2Axiom(qF) ∧ qF(train,tracks) ⊃ ¬safe-to-cross(tracks)%1,

where qF is a predicate parameter that can be replaced by any
predicate expression that can be written in the language being
used.  If we can find a qF that makes the left hand side of
({eq a2}) provable, then we can be sure that %2Axiom(on)%1
together with %2on(train,tracks)%1 has a model assuming that
%2Axiom(on)%1 is consistent.  Therefore, the schema ({eq a2})
is essentially a consequence of the McDermott-Doyle formula
({eq a1}).  The converse isn't true.  A predicate symbol may have
a model without there being an explicit formula realizing it.
I believe, however, that the schema is usable in all cases
where the McDermott-Doyle or Reiter formalisms can be practically
applied, and, in particular, to all the examples in their papers.

	(If one wants a counter-example to the usability of the schema,
one might look at the membership relation  of set theory with
the finitely axiomatized
Goedel-Bernays set theory as the axiom.  Instantiating qF in this case
would amount to giving an internal model of set theory, and
this is possible only in a stronger theory).

	It appears that such use of schemata amounts
to importing part of the model theory of a subject into the
theory itself.  It looks useful and even essential for common
sense reasoning, but its logical properties are not obvious.

	We can also go frankly to second order logic and write

!!a3:	%2∃qF.(Axiom(qF) ∧ on(train,tracks) ⊃ ¬safe-to-cross(tracks))%1.

Second order reasoning, which might be in set theory or a formalism
admitting concepts as objects rather than in second order logic,
seems to have the advantage that some of the predicate and function
symbols may be left fixed and others imitated by predicate parameters.
This allows us to say something like, "For any interpretation of
⊗P and ⊗Q satisfying the axiom ⊗A, if there is an interpretation in
which ⊗R and ⊗S satisfy the additional axiom ⊗A', then it is unsafe
to cross the tracks".  This maybe needed to express common sense
non-monotonic reasoning and it seems more powerful than any of
the above-mentioned non-monotonic formalisms including circumscription.

	The train example is a non-normal default in Reiter's sense,
because we cannot conclude that the train is on the tracks
in the absence of evidence to the contrary.  Indeed, suppose that we want to
wait for and catch a train at a station across the tracks.  If there might
be a train coming we will take a bridge rather than a shortcut across
the tracks, but we don't want to jump to the conclusion that there is a train,
because then we would think we were too late and give up trying to catch it.
The statement can be reformulated as a normal default by writing

!!a4:	%2M ¬safe-to-cross(tracks) ⊃ ¬safe-to-cross(tracks)%1,

but this is unlikely to be equivalent in all cases and the non-normal
expression seems to express better the common sense facts.

	Like normal defaults, circumscription doesn't deal with
possibility directly, and a circumscriptive treatment of the train
problem would involve circumscribing %2safe-to-cross(tracks)%1 in
the set of axioms.  It therefore might not be completely satisfactory.

.skip 2
Addendum to References:

%3McDermott, Drew and Jon Doyle (1980): "Non-Monotonic Logic I",
%2Artificial Intelligence%1, this issue.